/* Bogor: An Extensible and Highly-Modular Model Checking Framework
 * Copyright (c) 2002-2005 Kansas State University
 *
 * This software is licensed using the SAnToS Laboratory Open Academic License.
 * You should have received a copy of the License in the top directory of this
 * software distribution package. If not, then write to
 * SAnToS Laboratory, 234 Nichols Hall, Manhattan, KS 66506, USA.
 *
 * The SAnToS Laboratory homepage is located at http://www.cis.ksu.edu/santos.
 * The Bogor homepage is located at http://bogor.projects.cis.ksu.edu.
 */
package edu.ksu.cis.projects.bogor;

import java.io.PrintWriter;
import java.lang.reflect.Method;
import java.util.ArrayList;
import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Properties;
import java.util.Set;

import edu.ksu.cis.projects.bogor.ast.transform.ISystemTransformer;
import edu.ksu.cis.projects.bogor.module.ConfigurationMessages;
import edu.ksu.cis.projects.bogor.module.DefaultMessageStore;
import edu.ksu.cis.projects.bogor.module.IActionTaker;
import edu.ksu.cis.projects.bogor.module.IBacktrackingInfoFactory;
import edu.ksu.cis.projects.bogor.module.ICounterExampleWriter;
import edu.ksu.cis.projects.bogor.module.IExpEvaluator;
import edu.ksu.cis.projects.bogor.module.IListener;
import edu.ksu.cis.projects.bogor.module.IMessageStore;
import edu.ksu.cis.projects.bogor.module.IModule;
import edu.ksu.cis.projects.bogor.module.IProgressManager;
import edu.ksu.cis.projects.bogor.module.ISchedulingStrategist;
import edu.ksu.cis.projects.bogor.module.ISearcher;
import edu.ksu.cis.projects.bogor.module.IStateFactory;
import edu.ksu.cis.projects.bogor.module.IStateManager;
import edu.ksu.cis.projects.bogor.module.ITransformer;
import edu.ksu.cis.projects.bogor.module.IValueFactory;
import edu.ksu.cis.projects.bogor.symboltable.ExtSymbolTable;
import edu.ksu.cis.projects.bogor.symboltable.SymbolTable;
import edu.ksu.cis.projects.bogor.util.FileMessage;
import edu.ksu.cis.projects.bogor.util.Util;

/**
 * @author <a href="mailto:robby@cis.ksu.edu">Robby </a>
 * @author <a href="mailto:matt@cis.ksu.edu">Matt Hoosier </a>
 * @version CVS $Revision: 1.30 $ $Date: 2005/08/12 18:54:50 $
 */
public class DefaultBogorConfiguration
    implements IBogorConfiguration
{
    // ~ Instance variables
    // .....................................................

    // .....................................................
    protected String filename;

    protected SymbolTable symbolTable;

    protected PrintWriter pw;

    protected IActionTaker at;

    protected IBacktrackingInfoFactory bif;

    protected ICounterExampleWriter cew;

    protected IExpEvaluator ee;

    protected IProgressManager pm;

    protected ISchedulingStrategist ss;

    protected ISearcher sr;

    protected IStateFactory sf;

    protected IStateManager sm;

    protected ITransformer tr;

    protected IValueFactory vf;

    protected ArrayList<IListener> listeners;

    protected HashMap<ExtSymbolTable, IModule> extTable;

    protected Properties configuration;

    protected Set<String> copyrightTextSet;

    protected Map<String, IModule> instanceTable;

    protected IMessageStore firstTimeInitializationMessage;

    /**
     * Cache of singleton instances created by
     * {@link #createCheckedInstance(Class, String, Collection)}.
     */
    protected HashMap<String, Object> checkedInstanceCache = new HashMap<String, Object>();

    protected Map<String, Object> externalObjectMap;

    // ~ Methods
    // ................................................................

    // ................................................................
    public void setActionTaker(IActionTaker at)
    {
        assert (at != null);
        this.at = at;
    }

    public IActionTaker getActionTaker()
    {
        return at;
    }

    public void setBacktrackingInfoFactory(IBacktrackingInfoFactory bif)
    {
        assert (bif != null);
        this.bif = bif;
    }

    public IBacktrackingInfoFactory getBacktrackingInfoFactory()
    {
        return bif;
    }

    public Properties getConfiguration()
    {
        return configuration;
    }

    public void setCounterExampleWriter(ICounterExampleWriter cew)
    {
        assert (cew != null);
        this.cew = cew;
    }

    public ICounterExampleWriter getCounterExampleWriter()
    {
        return cew;
    }

    public void setExpEvaluator(IExpEvaluator ee)
    {
        assert (ee != null);
        this.ee = ee;
    }

    public IExpEvaluator getExpEvaluator()
    {
        return ee;
    }

    public Map<ExtSymbolTable, IModule> getExtTable()
    {
        return extTable;
    }

    public IModule getExtensionModule(String extId)
    {
        return (IModule) instanceTable.get(extId);
    }

    public String getFilename()
    {
        return filename;
    }

    public Object getModuleInstance(
        String className,
        Class interfaceClass,
        Collection<FileMessage> errors)
    {
        int oldErrorCount = errors.size();

        Object result = createCheckedInstance(interfaceClass, className, errors);

        if (errors.size() > oldErrorCount)
        {
            return null;
        }
        else
        {
            return result;
        }
    }

    public Object getPluginClassInstance(
        String className,
        Class interfaceType,
        Collection<FileMessage> errors)
    {
        return getPluginClassInstance(null, /*
                                             * this parameter not used in our
                                             * implementation
                                             */
        className, interfaceType, errors);
    }

    public Object getPluginClassInstance(
        Properties config,
        String className,
        Class interfaceType,
        Collection<FileMessage> errors)
    {
        return createCheckedInstance(interfaceType, className, errors);
    }

    public PrintWriter getPrintWriter()
    {
        return pw;
    }

    public void setProgressManager(IProgressManager pm)
    {
        assert (pm != null);
        this.pm = pm;
    }

    public IProgressManager getProgressManager()
    {
        return pm;
    }

    public void setSchedulingStrategist(ISchedulingStrategist ss)
    {
        assert (ss != null);
        this.ss = ss;
    }

    public ISchedulingStrategist getSchedulingStrategist()
    {
        return ss;
    }

    public void setSearcher(ISearcher sr)
    {
        assert (sr != null);
        this.sr = sr;
    }

    public ISearcher getSearcher()
    {
        return sr;
    }

    public void setStateFactory(IStateFactory sf)
    {
        assert (sf != null);
        this.sf = sf;
    }

    public IStateFactory getStateFactory()
    {
        return sf;
    }

    public void setStateManager(IStateManager sm)
    {
        assert (sm != null);
        this.sm = sm;
    }

    public IStateManager getStateManager()
    {
        return sm;
    }

    public SymbolTable getSymbolTable()
    {
        return symbolTable;
    }

    public ISystemTransformer[] getSystemTransformers(
        Properties configuration,
        Collection<FileMessage> errors)
    {
        ArrayList<ISystemTransformer> result = new ArrayList<ISystemTransformer>();
        String transformerList = configuration
            .getProperty(ISystemTransformer.class.getName());

        if (transformerList == null)
        {
            return new ISystemTransformer[0];
        }

        for (String className : Util.splitCommaSeparatedList(transformerList))
        {
            ISystemTransformer obj = (ISystemTransformer) createCheckedInstance(
                ISystemTransformer.class,
                className,
                errors);

            if (obj != null)
            {
                result.add(obj);
            }
        }

        return result.toArray(new ISystemTransformer[result.size()]);
    }

    public void setTransformer(ITransformer tr)
    {
        assert (tr != null);
        this.tr = tr;
    }

    public ITransformer getTransformer()
    {
        return tr;
    }

    public void setValueFactory(IValueFactory vf)
    {
        assert (vf != null);
        this.vf = vf;
    }

    public IValueFactory getValueFactory()
    {
        return vf;
    }

    public List<IListener> getListeners()
    {
        return listeners;
    }

    public IMessageStore connect()
    {
        DefaultMessageStore result = new DefaultMessageStore();

        result.merge(vf.connect(this));
        result.merge(sf.connect(this));
        result.merge(sm.connect(this));
        result.merge(ss.connect(this));
        result.merge(ee.connect(this));
        result.merge(bif.connect(this));
        result.merge(at.connect(this));
        result.merge(tr.connect(this));
        result.merge(sr.connect(this));
        result.merge(cew.connect(this));
        result.merge(pm.connect(this));

        for (IListener listener : listeners)
        {
            result.merge(listener.connect(this));
        }

        for (IModule m : instanceTable.values())
        {
            result.merge(m.connect(this));
        }

        return result;
    }

    public void dispose()
    {
        HashSet<IModule> disposedModules = new HashSet<IModule>();

        configuration = null;

        if (vf != null && !disposedModules.contains(vf))
        {
            disposedModules.add(vf);
            vf.dispose();
            vf = null;
        }

        if (sf != null && !disposedModules.contains(sf))
        {
            disposedModules.add(sf);
            sf.dispose();
            sf = null;
        }

        if (sm != null && !disposedModules.contains(sm))
        {
            disposedModules.add(sm);
            sm.dispose();
            sm = null;
        }

        if (ss != null && !disposedModules.contains(ss))
        {
            disposedModules.add(ss);
            ss.dispose();
            ss = null;
        }

        if (ee != null && !disposedModules.contains(ee))
        {
            disposedModules.add(ee);
            ee.dispose();
            ee = null;
        }

        if (bif != null && !disposedModules.contains(bif))
        {
            disposedModules.add(bif);
            bif.dispose();
            bif = null;
        }

        if (at != null && !disposedModules.contains(at))
        {
            disposedModules.add(at);
            at.dispose();
            at = null;
        }

        if (tr != null && !disposedModules.contains(tr))
        {
            disposedModules.add(tr);
            tr.dispose();
            tr = null;
        }

        if (sr != null && !disposedModules.contains(sr))
        {
            disposedModules.add(sr);
            sr.dispose();
            sr = null;
        }

        if (cew != null && !disposedModules.contains(cew))
        {
            disposedModules.add(cew);
            cew.dispose();
            cew = null;
        }

        if (listeners != null)
        {
            for (IListener listener : listeners)
            {
                if (!disposedModules.contains(listener))
                {
                    disposedModules.add(listener);
                    listener.dispose();
                }
            }

            listeners.clear();
            listeners = null;
        }

        filename = null;

        if (extTable != null)
        {
            for (IModule m : extTable.values())
            {
                if (!disposedModules.contains(m))
                {
                    disposedModules.add(m);
                    m.dispose();
                }
            }

            extTable.clear();
            extTable = null;
        }

        pw = null;

        if (checkedInstanceCache != null)
        {
            checkedInstanceCache.clear();
            checkedInstanceCache = null;
        }

        disposedModules.clear();
    }

    public IMessageStore initialize(
        SymbolTable symbolTable,
        IProgressManager pm,
        PrintWriter pw,
        Properties configuration,
        Map<String, Object> externalObjectMap)
    {
        if (firstTimeInitializationMessage != null)
        {
            return firstTimeInitializationMessage;
        }

        this.firstTimeInitializationMessage = new DefaultMessageStore();
        this.symbolTable = symbolTable;
        this.filename = symbolTable.getFilename();
        this.pm = pm;
        this.pw = pw;
        this.configuration = configuration;
        this.externalObjectMap = externalObjectMap;

        ArrayList<FileMessage> errors = new ArrayList<FileMessage>();

        at = (IActionTaker) createInstance(IActionTaker.class, errors);
        bif = (IBacktrackingInfoFactory) createInstance(
            IBacktrackingInfoFactory.class,
            errors);
        cew = (ICounterExampleWriter) createInstance(
            ICounterExampleWriter.class,
            errors);
        ee = (IExpEvaluator) createInstance(IExpEvaluator.class, errors);
        ss = (ISchedulingStrategist) createInstance(
            ISchedulingStrategist.class,
            errors);
        sr = (ISearcher) createInstance(ISearcher.class, errors);
        sf = (IStateFactory) createInstance(IStateFactory.class, errors);
        sm = (IStateManager) createInstance(IStateManager.class, errors);
        tr = (ITransformer) createInstance(ITransformer.class, errors);
        vf = (IValueFactory) createInstance(IValueFactory.class, errors);

        if (configuration.containsKey(IListener.class.getName()))
        {
            List<String> classes = Util.splitCommaSeparatedList(configuration
                .getProperty(IListener.class.getName()));

            listeners = new ArrayList<IListener>(classes.size());

            for (String listenerClass : classes)
            {
                IListener l = (IListener) createCheckedInstance(
                    IListener.class,
                    listenerClass,
                    errors);

                if (l != null)
                {
                    listeners.add(l);
                }
            }
        }
        else
        {
            listeners = new ArrayList<IListener>(0);
        }

        int size = errors.size();

        IMessageStore returnValue = (size > 0) ? new DefaultMessageStore(
            errors,
            new ArrayList<FileMessage>()) : initialize();
        firstTimeInitializationMessage.merge(returnValue);
        return returnValue;
    }

    protected Object createCheckedInstance(
        Class interfaceClass,
        String className,
        Collection<FileMessage> errors)
    {
        try
        {
            Object result = checkedInstanceCache.get(className);

            if (result != null)
            {
                if (!interfaceClass.isInstance(result))
                {
                    errors.add(FileMessage.buildMessage(
                        ConfigurationMessages.INTERFACE_NOT_IMPLEMENTED,
                        new String[]
                            {
                                className, interfaceClass.getName()
                            }));

                    return null;
                }
                else
                {
                    return result;
                }
            }

            result = Class.forName(className).newInstance();

            if (result != null)
            {
                checkedInstanceCache.put(className, result);
            }

            if (interfaceClass.isInstance(result))
            {
                return result;
            }
            else
            {
                errors.add(FileMessage.buildMessage(
                    ConfigurationMessages.INTERFACE_NOT_IMPLEMENTED,
                    new String[]
                        {
                            className, interfaceClass.getName()
                        }));
            }
        }
        catch (ClassNotFoundException cnfe)
        {
            errors.add(FileMessage.buildMessage(
                ConfigurationMessages.CLASS_NOT_FOUND,
                new String[]
                    {
                        cnfe.getMessage()
                    }));
        }
        catch (IllegalAccessException iae)
        {
            errors.add(FileMessage.buildMessage(
                ConfigurationMessages.INACCESSIBLE_EXT_MODULE,
                new String[]
                    {
                        iae.getMessage()
                    }));
        }
        catch (InstantiationException ie)
        {
            errors.add(FileMessage.buildMessage(
                ConfigurationMessages.COULDNT_INSTANTIATE,
                new String[]
                    {
                        ie.getMessage()
                    }));
        }

        return null;
    }

    protected Object createInstance(
        Class interfaceClass,
        ArrayList<FileMessage> errors)
    {
        String className = configuration.getProperty(interfaceClass.getName());

        if (className == null)
        {
            errors.add(FileMessage.buildMessage(
                ConfigurationMessages.NO_CONFIG,
                new String[]
                    {
                        interfaceClass.getName()
                    }));

            return null;
        }
        else
        {
            return createCheckedInstance(interfaceClass, className, errors);
        }
    }

    protected IMessageStore initialize()
    {
        copyrightTextSet = new HashSet<String>();
        extTable = new HashMap<ExtSymbolTable, IModule>();

        DefaultMessageStore moduleOptsMessages = new DefaultMessageStore();

        printCopyrightAndSetOptions(
            at.getCopyrightNotice(),
            at,
            IActionTaker.class.getName(),
            configuration,
            moduleOptsMessages);
        printCopyrightAndSetOptions(
            bif.getCopyrightNotice(),
            bif,
            IBacktrackingInfoFactory.class.getName(),
            configuration,
            moduleOptsMessages);
        printCopyrightAndSetOptions(
            cew.getCopyrightNotice(),
            cew,
            ICounterExampleWriter.class.getName(),
            configuration,
            moduleOptsMessages);
        printCopyrightAndSetOptions(
            ee.getCopyrightNotice(),
            ee,
            IExpEvaluator.class.getName(),
            configuration,
            moduleOptsMessages);
        printCopyrightAndSetOptions(
            ss.getCopyrightNotice(),
            ss,
            ISchedulingStrategist.class.getName(),
            configuration,
            moduleOptsMessages);
        printCopyrightAndSetOptions(
            sr.getCopyrightNotice(),
            sr,
            ISearcher.class.getName(),
            configuration,
            moduleOptsMessages);
        printCopyrightAndSetOptions(
            sf.getCopyrightNotice(),
            sf,
            IStateFactory.class.getName(),
            configuration,
            moduleOptsMessages);
        printCopyrightAndSetOptions(
            sm.getCopyrightNotice(),
            sm,
            IStateManager.class.getName(),
            configuration,
            moduleOptsMessages);
        printCopyrightAndSetOptions(
            tr.getCopyrightNotice(),
            tr,
            ITransformer.class.getName(),
            configuration,
            moduleOptsMessages);
        printCopyrightAndSetOptions(
            vf.getCopyrightNotice(),
            vf,
            IValueFactory.class.getName(),
            configuration,
            moduleOptsMessages);

        for (IListener listener : listeners)
        {
            printCopyrightAndSetOptions(
                listener.getCopyrightNotice(),
                listener,
                IListener.class.getName(),
                configuration,
                moduleOptsMessages);
        }

        Map<String, ExtSymbolTable> extTable = symbolTable
            .getExpActionExtTable();
        ArrayList<FileMessage> errors = new ArrayList<FileMessage>();
        ArrayList<FileMessage> warnings = new ArrayList<FileMessage>();
        instanceTable = new HashMap<String, IModule>();

        if (extTable.size() != 0)
        {
            for (ExtSymbolTable est : extTable.values())
            {
                String extId = est.getExtId();
                String className = est.getClassName();

                try
                {
                    Class c = Class.forName(className);
                    String methodName = est.getId();
                    Method m = c.getMethod(methodName, EXT_OP_ARG_TYPES);
                    Class rType = m.getReturnType();

                    if (est.getExpType() == null)
                    {
                        boolean returnTypeOk;

                        if (LEGACY_ACTION_DEF_EXT_OP_RETURN_TYPE
                            .isAssignableFrom(rType)
                            && !ACTION_DEF_EXT_OP_RETURN_TYPE
                                .isAssignableFrom(rType))
                        {
                            returnTypeOk = true;

                            warnings.add(FileMessage
                                .buildMessage(
                                    ConfigurationMessages.LEGACY_RETURN_TYPE,
                                    new String[]
                                        {
                                            className,
                                            methodName,
                                            ACTION_DEF_EXT_OP_RETURN_TYPE
                                                .getName(),
                                            LEGACY_ACTION_DEF_EXT_OP_RETURN_TYPE
                                                .getName()
                                        }));
                        }
                        else if (ACTION_DEF_EXT_OP_RETURN_TYPE
                            .isAssignableFrom(rType))
                        {
                            returnTypeOk = true;
                        }
                        else
                        {
                            returnTypeOk = false;
                            errors.add(FileMessage.buildMessage(
                                ConfigurationMessages.WRONG_RETURN_TYPE,
                                new String[]
                                    {
                                        className, methodName,
                                        ACTION_DEF_EXT_OP_RETURN_TYPE.getName()
                                    }));
                        }

                        if (returnTypeOk)
                        {
                            IModule extInstance = instanceTable.get(extId);

                            ArrayList<FileMessage> extInstanceErrors = new ArrayList<FileMessage>();

                            if (extInstance == null)
                            {
                                extInstance = (IModule) createCheckedInstance(
                                    c,
                                    className,
                                    extInstanceErrors);
                            }

                            if ((extInstance != null)
                                && extInstanceErrors.isEmpty())
                            {
                                printCopyrightAndSetOptions(
                                    extInstance.getCopyrightNotice(),
                                    extInstance,
                                    extId,
                                    configuration,
                                    moduleOptsMessages);
                                instanceTable.put(extId, extInstance);
                                getExtTable().put(est, extInstance);
                            }
                            else
                            {
                                errors.addAll(extInstanceErrors);
                            }

                            est.setMethod(m);
                        }
                    }
                    else
                    {
                        if (!EXP_DEF_EXT_OP_RETURN_TYPE.isAssignableFrom(rType))
                        {
                            errors.add(FileMessage.buildMessage(
                                ConfigurationMessages.WRONG_RETURN_TYPE,
                                new String[]
                                    {
                                        className, methodName,
                                        EXP_DEF_EXT_OP_RETURN_TYPE.getName()
                                    }));
                        }
                        else
                        {
                            IModule extInstance = instanceTable.get(extId);

                            ArrayList<FileMessage> extInstanceErrors = new ArrayList<FileMessage>();

                            if (extInstance == null)
                            {
                                extInstance = (IModule) createCheckedInstance(
                                    c,
                                    className,
                                    extInstanceErrors);
                            }

                            if ((extInstance != null)
                                && extInstanceErrors.isEmpty())
                            {
                                printCopyrightAndSetOptions(
                                    extInstance.getCopyrightNotice(),
                                    extInstance,
                                    extId,
                                    configuration,
                                    moduleOptsMessages);
                                instanceTable.put(extId, extInstance);
                                getExtTable().put(est, extInstance);
                            }
                            else
                            {
                                errors.addAll(extInstanceErrors);
                            }

                            est.setMethod(m);
                        }
                    }
                }
                catch (ClassNotFoundException cnfe)
                {
                    errors.add(FileMessage.buildMessage(
                        ConfigurationMessages.MOD_NOT_FOUND,
                        new String[]
                            {
                                cnfe.getMessage()
                            }));
                }
                catch (ClassCastException cce)
                {
                    errors.add(FileMessage.buildMessage(
                        ConfigurationMessages.INVALID_EXT_MOD,
                        new String[]
                            {
                                cce.getMessage()
                            }));
                }
                catch (NoSuchMethodException nsme)
                {
                    errors.add(FileMessage.buildMessage(
                        ConfigurationMessages.METHOD_NOT_FOUND,
                        new String[]
                            {
                                nsme.getMessage()
                            }));
                }
            }
        }

        // TODO: need to check for createDefaultValue for ptypedef
        moduleOptsMessages.merge(new DefaultMessageStore(errors, warnings));
        if (moduleOptsMessages.getErrorCount() > 0)
        {
            return moduleOptsMessages;
        }

        IMessageStore connectMessages = connect();
        connectMessages.merge(moduleOptsMessages);
        return connectMessages;
    }

    protected void printCopyrightAndSetOptions(
        String text,
        IModule m,
        String key,
        Properties configuration,
        IMessageStore moduleOptsMessages)
    {
        if (text != null)
        {
            if (!copyrightTextSet.contains(text))
            {
                pw.println(text);
                pw.println();
                pw.flush();
                copyrightTextSet.add(text);
            }
        }

        moduleOptsMessages.merge(m.setOptions(key, configuration));
    }

    /**
     * Trivial implementation; always returns a zero-length list.
     * 
     * @param interfaceType
     * @return
     */
    public List<Class> getKnownImplementingClasses(Class< ? > interfaceType)
    {
        return new ArrayList<Class>(0);
    }

    public Map<String, Object> getExternalObjectMap()
    {
        return externalObjectMap;
    }
}
